(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_56_9 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EDX_8_93_5 () (_ BitVec 32))
(declare-fun R_EAX_5_75_4 () (_ BitVec 32))
(declare-fun R_EBX_6_61_3 () (_ BitVec 32))
(declare-fun R_EBP_0_65_2 () (_ BitVec 32))
(declare-fun R_ESP_1_58_1 () (_ BitVec 32))
(assert (let ((?v_0 (bvsub (bvsub R_ESP_1_58_1 (_ bv4 32)) (_ bv4 32)))) (let ((?v_10 (bvadd (bvadd ?v_0 (_ bv4 32)) (_ bv4 32))) (?v_1 (bvsub (bvsub ?v_0 (_ bv4 32)) (_ bv4 32))) (?v_2 (store (store (store (store mem_35_56_9 (bvadd ?v_0 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_65_2 (_ bv24 32)))) (bvadd ?v_0 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_65_2 (_ bv16 32)))) (bvadd ?v_0 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_65_2 (_ bv8 32)))) (bvadd ?v_0 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_65_2)))) (let ((?v_5 (store (store (store (store ?v_2 (bvadd ?v_1 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_61_3 (_ bv24 32)))) (bvadd ?v_1 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_61_3 (_ bv16 32)))) (bvadd ?v_1 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_61_3 (_ bv8 32)))) (bvadd ?v_1 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_61_3)))) (let ((?v_7 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (_ bv134550276 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (_ bv134550277 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (_ bv134550278 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (_ bv134550279 32))) (_ bv24 32)))) (?v_3 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_2 (_ bv134550272 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134550273 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134550274 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134550275 32))) (_ bv24 32))))) (let ((?v_6 (bvadd R_EAX_5_75_4 ?v_3))) (let ((?v_15 (bvand (concat (_ bv0 31) (ite (bvult ?v_6 R_EAX_5_75_4) (_ bv1 1) (_ bv0 1))) (_ bv1 32)))) (let ((?v_12 (bvadd (bvadd R_EDX_8_93_5 ?v_7) ?v_15)) (?v_4 (bvadd ?v_6 ?v_3))) (let ((?v_8 (bvadd (bvadd ?v_12 ?v_7) (bvand (concat (_ bv0 31) (ite (bvult ?v_4 ?v_6) (_ bv1 1) (_ bv0 1))) (_ bv1 32))))) (let ((?v_9 (store (store (store (store (store (store (store (store (store ?v_5 (_ bv134550275 32) ((_ extract 7 0) (bvlshr ?v_4 (_ bv24 32)))) (_ bv134550274 32) ((_ extract 7 0) (bvlshr ?v_4 (_ bv16 32)))) (_ bv134550273 32) ((_ extract 7 0) (bvlshr ?v_4 (_ bv8 32)))) (_ bv134550272 32) ((_ extract 7 0) ?v_4)) (_ bv134550279 32) ((_ extract 7 0) (bvlshr ?v_8 (_ bv24 32)))) (_ bv134550278 32) ((_ extract 7 0) (bvlshr ?v_8 (_ bv16 32)))) (_ bv134550277 32) ((_ extract 7 0) (bvlshr ?v_8 (_ bv8 32)))) (_ bv134550276 32) ((_ extract 7 0) ?v_8)) (_ bv134550280 32) (_ bv1 8))) (?v_11 (bvsub R_EAX_5_75_4 ?v_6)) (?v_18 (bvxor R_EAX_5_75_4 ?v_6)) (?v_13 (ite (bvult R_EDX_8_93_5 ?v_12) (_ bv1 1) (_ bv0 1))) (?v_14 (bvsub R_EDX_8_93_5 ?v_12)) (?v_17 (bvand ?v_15 (_ bv1 32)))) (let ((?v_16 (bvxor (bvxor ?v_7 ?v_15) ?v_17))) (= (_ bv1 1) (bvand (ite (not (= (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_56_9 (bvadd R_ESP_1_58_1 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_56_9 (bvadd R_ESP_1_58_1 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_56_9 (bvadd R_ESP_1_58_1 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_56_9 (bvadd R_ESP_1_58_1 (_ bv3 32)))) (_ bv24 32))) (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_9 (bvadd ?v_10 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_9 (bvadd ?v_10 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_9 (bvadd ?v_10 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_9 (bvadd ?v_10 (_ bv3 32)))) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)) (bvand (bvnot ((_ extract 0 0) (concat (_ bv0 31) (bvor (ite (bvult R_EAX_5_75_4 ?v_6) (_ bv1 1) (_ bv0 1)) (ite (= ?v_11 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand ?v_18 (bvxor R_EAX_5_75_4 ?v_11)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand ((_ extract 0 0) (concat (_ bv0 31) (bvor ?v_13 (ite (= ?v_14 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (bvand (bvnot ((_ extract 0 0) (concat (_ bv0 31) ?v_13))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_EDX_8_93_5 ?v_12) (bvxor R_EDX_8_93_5 ?v_14)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_EDX_8_93_5 (bvxor ?v_16 (_ bv4294967295 32))) (bvxor R_EDX_8_93_5 (bvadd (bvadd R_EDX_8_93_5 ?v_16) ?v_17))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_EAX_5_75_4 (bvxor ?v_3 (_ bv4294967295 32))) ?v_18) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1)))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
